$\forall$$M$, $A$:MsgA, $a$:Id, $p$:($A$.state$\rightarrow$$A$.da(locl($a$))$\rightarrow$Prop). $M$.rframe($A$.pre $p$ for $a$) $\in$ Prop